perm filename LISP.AX[S79,JMC] blob sn#430496 filedate 1979-04-06 generic text, type T, neo UTF8
DIST_IF3: ∀x1 y1 x y z.if(x1,y1,if(x,y,z))=if(x,if(x1,y1,y),if(x1,y1,z))
DIST_IF2: ∀x1 z1 x y z.if(x1,if(x,y,z),z1)=if(x,if(x1,y,z1),if(x1,z,z1))
DIST_IF1: ∀y1 z1 x y z.if(if(x,y,z),y1,z1)=if(x,if(y,y1,z1),if(z,y1,z1))
DIST_IF0: ∀x y z.F(if(x,y,z))=if(x,F(y),F(z))
DIST_AND_OR: ∀x y x1 y1.(True ((x or y) and (x1 or y1))≡True ((x and x1) or ((x and y1) or ((y and x1) or (y and%
 y1)))))
DIST_OR_AND: ∀x y x1 y1.(True ((x and y) or (x1 and y1))≡True ((x or x1) and ((x or y1) and ((y or x1) and (y or%
 y1)))))
DEMORGAN2: ∀x y.not (x or y)=(not x and not y)
DEMORGAN1: ∀x y.not (x and y)=(not x or not y)
ASSOC_OR: ∀x y z.((x or y) or z)=(x or (y or z))
ASSOC_AND: ∀x y z.((x and y) and z)=(x and (y and z))
SYM_OR: ∀x y.(True (x or y)≡True (y or x))
SYM_AND: ∀x y.(True (x and y)≡True (y and x))
NOT_NOT: ∀x.(True not not x≡True x)
EQV_NOT: ∀x.(True not x≡¬True x)
EQ_NOT: ∀x.not x=IF True x THEN qNIL ELSE qT
EQV_OR: ∀x y.(True (x or y)≡(True x∨True y))
EQ_OR: ∀x y.(x or y)=IF True x THEN x ELSE y
EQV_AND: ∀x y.(True (x and y)≡(True x∧True y))
EQ_AND: ∀x y.(x and y)=IF True x THEN y ELSE qNIL≡∀x y.IF True x THEN y ELSE x=IF True x THEN y ELSE qNIL
EQV_EQUAL: ∀x y.(True (x equal y)≡x=y)
EQ_EQUAL: ∀x y.(x equal y)=IF x=y THEN qT ELSE qNIL
EQV_NULL: ∀x.(True null x≡NULL x)
EQ_NULL: ∀x.null x=IF NULL x THEN qT ELSE qNIL
EQV_ATOM: ∀x.(True atom x≡ATOM x)
EQ_ATOM: ∀x.atom x=IF ATOM x THEN qT ELSE qNIL
EQV_IF: ∀x y z.(True if(x,y,z)≡((True x∧True y)∨(¬True x∧True z)))
VAL_IF: ∀x y z.((True x⊃if(x,y,z)=y)∧(¬True x⊃if(x,y,z)=z))
EQ_IF: ∀x y z.if(x,y,z)=IF True x THEN y ELSE z
FALSITY: ¬True qNIL
TRUTH1: ∀x.(True x≡¬(x=qNIL))
TRUTH: ∀x.(¬(x=qNIL)≡True x)
S_NOT: ∀x.SEXP not x
NOT_DEF: ∀X.not X=if(X,qNIL,qT)
S_OR: ∀x y.SEXP (x or y)
OR_DEF: ∀X Y.(X or Y)=if(X,X,Y)
S_AND: ∀x y.SEXP (x and y)
AND_DEF: ∀X Y.(X and Y)=if(X,Y,X)
CREVERSE1_SUM: ∀u.creverse1 u=sum length u
CREV_LEN: ∀u v.crev(u,v)=length u
CREVERSE1_UU: ∀uu.creverse1 uu=(length uu+creverse1 cdr uu)
CREVERSE1_DEF: ∀u.creverse1 u=IF NULL u THEN 0 ELSE add1 cappend(reverse1 cdr u,cons(car u,qNIL))+creverse1 cdr %
u
CREV_UU_V: ∀uu v.crev(uu,v)=add1 crev(cdr uu,cons(car uu,v))
CREV_DEF: ∀u v.crev(u,v)=IF NULL u THEN 0 ELSE add1 crev(cdr u,cons(car u,v))
CREVERSE1_DF: ∀u.creverse1 u=if(null u,0,add1 cappend(reverse1 cdr u,cons(car u,qNIL))+creverse1 cdr u)
CREV_DF: ∀u v.crev(u,v)=if(null u,0,add1 crev(cdr u,cons(car u,v)))
CAPP_LEN: ∀u v.cappend(u,v)=length u
LENGTH_REV: ∀u.length reverse1 u=length u
LENGTH_UV: ∀u v.length (u*v)=(length u+length v)
LENGTH_CDR: ∀vv.sub1 length vv=length cdr vv
LENGTH_NIL: length qNIL=0
LENGTH_UU: ∀uu.length uu=add1 length cdr uu
LENGTH_DEF: ∀u.length u=IF NULL u THEN 0 ELSE add1 length cdr u
LENGTH_DF: ∀u.length u=if(null u,0,add1 length cdr u)
CAPPEND_NIL: ∀v.cappend(qNIL,v)=0
CAPPEND_UU: ∀uu v.cappend(uu,v)=add1 cappend(cdr uu,v)
CAPPEND_DEF: ∀u v.cappend(u,v)=IF NULL u THEN 0 ELSE add1 cappend(cdr u,v)
CAPPEND_DF: ∀u v.cappend(u,v)=if(null u,0,add1 cappend(cdr u,v))
SUM_NN1: ∀nn.sum nn=(sum sub1 nn+nn)
SUM_NN: ∀nn.sum nn=(nn+sum sub1 nn)
SUM_ZERO: sum 0=0
SUM_DEF: ∀n.sum n=IF n=0 THEN 0 ELSE n+sum sub1 n
SUM_DF: ∀n.sum n=if(n equal 0,0,n+sum sub1 n)
ARITH_: PLUS_: PLUS_1: ∀n.(0+n)=n
       PLUS_2: ∀m n.(add1 n+m)=add1 (n+m)
        TIMES_: TIMES_1: ∀n.(0⊗n)=0
                TIMES_2: ∀m n.(add1 n⊗m)=((n⊗m)+m)
FACTOR_RT: ∀l m n.((m⊗l)+(n⊗l))=((m+n)⊗l)
FACTOR_LF: ∀l m n.((l⊗m)+(l⊗n))=(l⊗(m+n))
DISTRIB_RT: ∀l m n.((m+n)⊗l)=((m⊗l)+(n⊗l))
DISTRIB_LF: ∀l m n.(l⊗(m+n))=((l⊗m)+(l⊗n))
COMMUTE_TIME: ∀m n.(m⊗n)=(n⊗m)
COMMUTE_PLUS: ∀m n.(m+n)=(n+m)
ASSOC_PLUS2: ∀l m n.((l+m)+n)=(l+(m+n))
ASSOC_PLUS1: ∀l m n.(l+(m+n))=((l+m)+n)
NOT_N_LE_N: ∀n.¬(n<n)
ZERO_LTE_N: ∀n.0≤n
LE_ADD1: ∀n.n<add1 n
LE_SUB1: ∀nn.sub1 nn<nn
LE_M_NN: ∀m nn.(m≤nn≡(m=nn∨m≤sub1 nn))
NN1_NEQ_NN: ∀nn.¬(sub1 nn=nn)
N_NEQ_N1: ∀n.¬(n=add1 n)
ADD1_NOT_ZERO: ∀n.¬(add1 n=0)
NN_NOT_ZERO: ∀nn.¬(nn=0)
CVI_INDUCTION: ∀n.(∀m.(m<n⊃PSI(m))⊃PSI(n))⊃∀n.PSI(n)
NUM_INDUCTION1: (PSI(0)∧∀nn.(PSI(sub1 nn)⊃PSI(nn)))⊃∀n.PSI(n)
NUM_INDUCTION: (PSI(0)∧∀nn.(PSI(sub1 nn)⊃PSI(nn)))⊃∀n.PSI(n)
ORDER: LEQ: ∀m n.(m≤n≡(m=n∨(¬(n=0)∧m≤sub1 n)))
       LE: ∀m n.(m<n≡(m≤n∧¬(m=n)))
       GEQ: ∀m n.(m≥n≡n≤m)
       GE: ∀m n.(m>n≡n<m)
NUMERALS: ONE: 1=add1 0
          TWO: 2=add1 1
ARITH: PLUS: PLUS1: ∀n.(n+0)=n
      PLUS2: ∀m n.(n+add1 m)=add1 (n+m)
       TIMES: TIMES1: ∀n.(n⊗0)=0
              TIMES2: ∀m n.(n⊗add1 m)=((n⊗m)+n)
NATNUM: POS: ∀n.(POSP n≡¬ZEROP n)
        ZER: ∀X.(ZEROP X≡X=0)
        SUB1: SUB11: ∀n.sub1 add1 n=n
              SUB12: ∀nn.add1 sub1 nn=nn
        ADD1: ∀m n.(add1 m=add1 n≡m=n)
APP_REV: ∀u v w.(rev(u,v)*w)=rev(u,v*w)
REV_REV_UVW: ∀u v w.rev(rev(u,v),w)=rev(v,u*w)
REV_APP: ∀u v w.rev(u*v,w)=rev(v,rev(u,w))
REV_REV: ∀u.reverse reverse u=u
REV_REV1: ∀u.reverse1 reverse1 u=u
REV_UV: ∀u v.reverse (u*v)=(reverse v*reverse u)
REV1_UV: ∀u v.reverse1 (u*v)=(reverse1 v*reverse1 u)
EQ_REV1: ∀u.reverse1 u=reverse u
EQ_REV: ∀u.reverse u=reverse1 u
EQ_REV: ∀u.reverse u=reverse1 u
REV1_X: ∀x.reverse1 cons(x,qNIL)=cons(x,qNIL)
REVERSE1_UU: ∀uu.reverse1 uu=(reverse1 cdr uu*cons(car uu,qNIL))
REVERSE1_DEF: ∀u.reverse1 u=IF NULL u THEN qNIL ELSE reverse1 cdr u*cons(car u,qNIL)
REV_UU_V: ∀uu v.rev(uu,v)=rev(cdr uu,cons(car uu,v))
REV_DEF: ∀u v.rev(u,v)=IF NULL u THEN v ELSE rev(cdr u,cons(car u,v))
REV1_DEF: ∀u v.rev1(u,v)=(reverse1 u*v)
REVERSE1_DF: ∀u.reverse1 u=if(null u,qNIL,reverse1 cdr u*cons(car u,qNIL))
REV_DF: ∀u v.rev(u,v)=if(null u,v,rev(cdr u,cons(car u,v)))
REVERSE_DEF: ∀u.reverse u=rev(u,qNIL)
APP_XU_V: ∀x u v.app(cons(x,u),v)=cons(x,app(u,v))
APP_ASS: ∀u v w.app(u,app(v,w))=app(app(u,v),w)
APP_ONE: ∀x v.app(cons(x,qNIL),v)=cons(x,v)
APP_NIL: ∀v.app(qNIL,v)=v
APP_XU_V: ∀x u v.app(cons(x,u),v)=cons(x,app(u,v))
APP_ASS: ∀u v w.app(u,app(v,w))=app(app(u,v),w)
APP_ONE: ∀x v.app(cons(x,qNIL),v)=cons(x,v)
APP_NIL: ∀v.app(qNIL,v)=v
ASSOC1_APPEND: ∀u v w.((u*v)*w)=(u*(v*w))
ASSOC_APPEND: ∀u v w.(u*(v*w))=((u*v)*w)
RID_APPEND: ∀u.(u*qNIL)=u
NE_APPEND_U_VV: ∀u vv.NELIST (u*vv)
NE_APPEND_UU_V: ∀uu v.NELIST (uu*v)
L_APPEND: ∀u v.LIST (u*v)
APPEND_XU_V: ∀x u v.(cons(x,u)*v)=cons(x,u*v)
APPEND_XV: ∀x v.(cons(x,qNIL)*v)=cons(x,v)
APPEND_NIL_V: ∀v.(qNIL*v)=v
APPEND_UU_V: ∀uu v.(uu*v)=cons(car uu,cdr uu*v)
APPEND_DEF: ∀u v.(u*v)=IF NULL u THEN v ELSE cons(car u,cdr u*v)
APPEND_DF: ∀u v.(u*v)=if(null u,v,cons(car u,cdr u*v))
APPEN_DF: ∀u v.(u*v)=if(null u,v,cons(car u,cdr u*v))
S_EQUAL: ∀x y.SEXP (x equal y)
EQUAL_DEF: ∀X Y.(X equal Y)=IF ¬SEXP X∨¬SEXP Y THEN undef ELSE IF X=Y THEN qT ELSE qNIL
S_NULL: ∀x.SEXP null x
NULL_DEF: ∀X.null X=IF ¬SEXP X THEN undef ELSE IF NULL X THEN qT ELSE qNIL
S_ATOM: ∀x.SEXP atom x
ATOM_DEF: ∀X.atom X=IF ¬SEXP X THEN undef ELSE IF ATOM X THEN qT ELSE qNIL
S_IF: ∀x y z.SEXP if(x,y,z)
IF_DEF: ∀X Y Z.if(X,Y,Z)=IF ¬SEXP X THEN undef ELSE IF ¬(X=qNIL) THEN Y ELSE Z
ALL_X: (∀a.PHI(a)∧∀xx.PHI(xx))⊃∀x.PHI(x)
ALL_U: (PHI(qNIL)∧∀uu.PHI(uu))⊃∀u.PHI(u)
IF_X_ATOM: ∀x.(IF ATOM x THEN qT ELSE qNIL=qNIL≡¬ATOM x)
IF_U_NIL: ∀u.(IF u=qNIL THEN qT ELSE qNIL=qNIL≡¬(u=qNIL))
XX_NOT_A: ∀xx a.¬(xx=a)
XX_NOT_ATOM: ∀xx.¬ATOM xx
UU_NOT_NIL: ∀uu.¬(uu=qNIL)
CONS_1_1: ∀x y x1 y1.(cons(x,y)=cons(x1,y1)≡(x=x1∧y=y1))
EQSEXP: ∀xx yy.((car xx=car yy∧cdr xx=cdr yy)≡xx=yy)
T_NOT_NIL: ¬(qT=qNIL)
SEXPINDUCTION: (∀a.PHI(a)∧∀xx.((PHI(car xx)∧PHI(cdr xx))⊃PHI(xx)))⊃∀x.PHI(x)
LISTINDUCTION: (PHI(qNIL)∧∀uu.(PHI(cdr uu)⊃PHI(uu)))⊃∀u.PHI(u)
SEXP: BOTTOMAX: BOTTOMAX1: ∀X.(BOTTOM X≡X=undef)
          BOTTOMAX2: ¬SEXP undef
      NULLAX: NULLAX1: ∀u.(ATOM u≡NULL u)
              NULLAX2: ∀X.(NULL X≡X=qNIL)
      PAIRAX: PAIRAX1: ∀x.(PAIR x≡¬ATOM x)
              PAIRAX2: ∀u.(NELIST u≡¬NULL u)
      CAR: ∀x y.car cons(x,y)=x
      CDR: ∀x y.cdr cons(x,y)=y
      CONS: ∀xx.cons(car xx,cdr xx)=xx